<,*>  AbMon{1} 

latex

Up	groups 1
Definitions of Statement	<,*>
Definitions	<,*>, t  T, x f y, x:A. B(x), IsEqFun(T;eq), P & Q, P  Q, , P  Q, P  Q, Assoc(T;op), Ident(T;op;id), Comm(T;op)
Lemmas	le int wf, eq int wf, mk abmonoid, assert of eq int, assert wf, iff functionality wrt iff